package preprocessor.absorption.extended;

import java.util.HashMap;
import java.util.HashSet;
import java.util.Map;
import java.util.Map.Entry;
import java.util.Set;

import algebra.rewriting.kfree.LangPd;

import option.KBVocabulary;

import preprocessor.Simplification;
//import preprocessor.absorption.Absorption;
//import preprocessor.absorption.BinaryAbsorptionGuarded;
//import preprocessor.absorption.RoleAbsorption;

import tableaux.Completion;
import utils.exception.AbsorptionException;
import utils.exception.ConceptException;
import utils.exception.CoreReasoningException;
//import utils.exception.CoreReasoningException;
import utils.exception.TypeException;
//import entities.Assertion;
//import entities.Assertion;
//import entities.ConceptAssertion;
//import entities.RoleAssertion;
//import entities.ConceptAssertion;
import entities.Individual;
import entities.axiom.ConceptAxiom;
import entities.axiom.InclusionAxiom;
//import entities.RoleAssertion;
import entities.concept.AndConcept;
import entities.concept.NaryConcept;
import entities.concept.NotConcept;
import entities.concept.OrConcept;
import entities.concept.UniversalConcept;
import entities.concept.AtomicConcept;
import entities.concept.Concept;
import entities.concept.DomainConcept;
import entities.concept.ExistsConcept;
import entities.concept.Nominal;
import entities.concept.PConcept;
import entities.role.Role;
import kb.ABox;
import kb.DescriptionLogicsKB;
import kb.RBox;
import kb.TBox;

/**
 * For a:A => (a and DEF_a) -> A For a,b:R => ( a and DEF_r) -> Ex r.(b and
 * DEF_b) ( b and DEF_r^) -> Ex r^.(a and DEF_a) If allowing full guarding, add
 * a: f=k => (a and DEF_f) -> f=k
 * 
 * @author j55wu
 * 
 */
public class AssertionConversion {
	private static Map<DescriptionLogicsKB, TBox> absorbedKBs = new HashMap<DescriptionLogicsKB, TBox>();
	private static final boolean verbose = false;
	private static Set<DomainConcept<?, ?>> definedFeatures = new HashSet<DomainConcept<?, ?>>();

	//whether to add Exists R.top -> C : degrade the performance
	public static final boolean addDomainRestrictionInBinaryPairs = false; 
	
	public static void clearCachedConversion() {
		absorbedKBs.clear();
		cachedConverts.clear();
		OptimizedUniversals.clearAllCache();
	}

	private static Map<Concept, PConcept> cachedConverts = new HashMap<Concept, PConcept>();

	
	
	public static TBox getConvertedTBox(DescriptionLogicsKB kb, Boolean cu) {
//		collectUniversal = cu;
		if (kb == null) {
			return null;
		}
		if (absorbedKBs.containsKey(kb)) {
			return absorbedKBs.get(kb);
		}
		// convert and store
//		long start = System.currentTimeMillis();
		TBox tb = null;
		try {
			tb = AssertionConversion.convert(kb.getTbox(), kb.getAbox());
		} catch (CoreReasoningException e) {
			e.printStackTrace();
		}
//		System.err.println("Conversion time in total (incl. optimization time): "
//				+ (System.currentTimeMillis() - start) / 1000.0);
		absorbedKBs.put(kb, tb);
		if (verbose) {
			System.out.println("Converted Tbox binary entries: "
					+ tb.getSpecialBinaryClass().getTbLimited().size());
			System.out.println("Unary entries: " + tb.getTu().size());
			System.out.println("GCIs: " + tb.getTg().size());
			System.out.println("Newly introduced internal concepts: "
					+ PConcept.getNumFrenshConcept());
			System.out.println("Newly introduced guarded concepts: "
					+ PConcept.getGuardedConcept().size());
		}
		cachedConverts.clear();
		return tb;
	}




	public static TBox convert(TBox tb, ABox ab) throws CoreReasoningException {
		TBox convertedTb = new TBox();
		//the convertedTb must include the original RBox
		convertedTb.setRBox(tb.getRoleBox());
		//if kfree testing is using the reasoning service, Tf must be copied as well
		if(LangPd.useStarToReplaceConstants && tb.getTf().size()>0){
			convertedTb.setTf(tb.getTf());
		}
		//
		definedFeatures.clear();
		//convert role axioms
		convertRoleAxiom(tb.getRoleBox(), convertedTb);
		// process ABox
		if (ab != null) {
			for (Entry<Individual, Concept> e : ab.getConceptAssertions()
					.entrySet()) {
				try {
					convertCAssertion(e.getKey(), e.getValue(), convertedTb);
				} catch (TypeException e1) {
					e1.printStackTrace();
				}
			}
		}
		//convert TBox
		//first normalize axioms to avoid disjunction on LHS or conjunction on RHS
		Set<InclusionAxiom> nax = TBox.allAxiomsAsInclusions(tb.getOriginalTBoxAxioms());
//		nax = TBox.elimLeftDisjunctionAxioms(nax);
//		nax = TBox.elimRightConjunctionAxioms(nax);
		for (ConceptAxiom ax : nax) {
			convertInclusionAxiom(ax, convertedTb);
		}
//		// process RA
		if (OptimizedRestrictions.OptimizeUR && ab != null) {
			OptimizedUniversals.allRAs.putAll(ab.getRoleAssertions());
		}
		if (ab != null) {
			for (Entry<Individual, HashMap<Role, HashSet<Individual>>> e : ab
					.getRoleAssertions().entrySet()) {
				for (Entry<Role, HashSet<Individual>> ee : e.getValue()
						.entrySet()) {
					for (Individual b : ee.getValue()) {
						convertRAssertion(e.getKey(), ee.getKey(), b,
								convertedTb);
					}
				}
			}
		}

//		if (OptimizedUniversals.OptimizeUR && !collectUniversal) {
//			System.err
//					.println("Skipped RAs: " + AssertionConversion.skippedRAs);
//		}
		// add all GCIs
		addGCIToConvertedTb(convertedTb);
		DefGCIs.clear();
		return convertedTb;
	}

	//given C->D, convert to TOP-> ~C or D, NNF assumed
	private static void convertInclusionAxiom(ConceptAxiom ax, TBox convertedTb) 
			throws CoreReasoningException {
		Set<Concept> disjuncts = Concept.reduceToDisjuncts(Simplification.NNF(ax.getRHS(), false));
		if(!ax.getLHS().isTop()){
			disjuncts.addAll(Concept.reduceToDisjuncts(Simplification.NNF(ax.getLHS(), true)));
		}
		if(disjuncts.size() == 1){
			//consider whether a domain/range restriction, i.e., top->all R (or R-).C
			Concept uni = disjuncts.iterator().next();
			if(uni instanceof UniversalConcept){
				//this is a domain/range axiom
				UniversalConcept uc = (UniversalConcept) uni;
				Role r = uc.getRole();
				Concept newfiller = convertConcept(uc.getFiller(), false, convertedTb);
				r.setRange(newfiller);
				return;
			}else if(OptimizedRestrictions.OptimizeEx && uni instanceof ExistsConcept){
				//Top -> some R.C
				ExistsConcept ec = (ExistsConcept) uni;
				Concept newfiller = convertConcept(ec.getFiller(), false, convertedTb);
				ec = new ExistsConcept(ec.getRole(), newfiller);
				collectExists(KBVocabulary.CONCEPT_TOP, ec);
			}
		}else if(disjuncts.size() == 2){
			//consider if this is a valid universal, 
			//i.e. (~)A -> all R. (~)B, i.e., top-> (~)A OR all R. (~)B
			Concept l =null;
			UniversalConcept r = null;
			ExistsConcept rec = null;
			for(Concept C: disjuncts){
				//one is literal, the other is a valid universal
				if(C.isLiteral()){
					l = C;
				}
				if(C instanceof UniversalConcept){
					if(validUseOfUniversal(C)){
						r = (UniversalConcept) C;
						continue;
					}else{
						UniversalConcept uc = (UniversalConcept) C;
						if(!uc.getFiller().isBot()){
							//not a domain/range restriction, then it is a general Forall R.C
							r = (UniversalConcept) convertUniversal(uc, false, convertedTb);
						}		
					}
				}
				if(OptimizedRestrictions.OptimizeEx && C instanceof ExistsConcept){
					if(validUseOfExists(C)){
						rec = (ExistsConcept) C;
						continue;
					}else{
						ExistsConcept ec = (ExistsConcept) C;
						rec = (ExistsConcept) convertExists(ec, false, convertedTb);		
					}
				}
			}
			if(l!=null){
				//Do not cache valid universals: incorrect
				Concept lhs = Simplification.NNF(l, true);
				if( r!=null){
//					if (!cachedConverts.containsKey(r)) {
						UniversalConcept rc = (UniversalConcept) r;
//						cachedConverts.put(r, (PConcept) lhs);
						addGCI(lhs, r, convertedTb);
						collectUniversals(lhs, rc);
						tboxGuardIntroduction(lhs, rc.getRole(), rc.getFiller(),
								convertedTb);
						return;
//					}
				}
				if(OptimizedRestrictions.OptimizeEx && rec!=null){
					addGCI(lhs, rec, convertedTb);
					collectExists(lhs, rec);
					return;
				}
			}

		}
		if(disjuncts.size() >= 2){
			UniversalConcept du = null;
			for(Concept C: disjuncts){
				if(C instanceof UniversalConcept){
					if(((UniversalConcept) C).getFiller().isBot()){
						du = (UniversalConcept) C;
						break;
					}
				}
			}
			//check if this is a domain restriction in the form : some R.TOP -> C
			//i.e., TOP-> all R. BOT \/ C, i.e., top->forall R-.C
			if(du != null){
				//a domain restriction!
				disjuncts.remove(du);
				Concept dc = Concept.getDisjunctiveConcept(disjuncts);
				dc = convertConcept(dc, true, convertedTb);
				Concept newfiller = convertConcept(dc, false, convertedTb);
				du.getRole().setDomain(newfiller);
			}else{
				//process as other non-standard axioms
				processAxiomsForUniversals(disjuncts, convertedTb);
			}
		}

		
	}
	
	private static void processAxiomsForUniversals(Set<Concept> disjuncts, TBox convertedTb) 
			throws CoreReasoningException{
		Set<Concept> oc = new HashSet<Concept>();
		for(Concept dis:disjuncts){
			oc.add(convertConcept(dis, true, convertedTb));
		}
		addGCI(KBVocabulary.CONCEPT_TOP, Concept.getDisjunctiveConcept(oc), convertedTb);
	}
	

	//for R < S, add DEF_S < DEF_R (the reverse is added!) for role hierarchy
	//for trans(R), add DEFr->forall R.DEFr and its inverse: DEFr- -> forall R-. DEFr-
	private static void convertRoleAxiom(RBox rb, TBox convertedTb){
		for(Role rl:rb.getSuperRolesMap().keySet()){
			for(Role rr:rb.getSuperRolesMap().get(rl)){
				if(rr.equals(rl)){
					continue;
				}
				addGCI(PConcept.newGuardPConcept(rr), PConcept.newGuardPConcept(rl), convertedTb);
			}
		}
		//add feature domains, for f:C, add DEF_f -> C
		for(Role f: rb.getFeatureDomain().keySet()){
			addGCI(PConcept.newGuardPConcept(f), rb.getFeatureDomain().get(f), convertedTb);
		}
		//add transitive roles
		for(Role r:rb.getTransRoles()){
			Role ir = rb.getInverseRole(r);
			PConcept defr = PConcept.newGuardPConcept(r);
			PConcept defir = PConcept.newGuardPConcept(ir);
			UniversalConcept rc = new UniversalConcept(r, defr), irc = new UniversalConcept(ir, defir);
			addGCI(defr, rc, convertedTb);
			addGCI(defir, irc, convertedTb);//inverse
//			addGCI(KBVocabulary.CONCEPT_TOP, new AndConcept(defr, defir), convertedTb);
		}
	}
	





	// public static void clearCachedConverts(){
	// cachedConverts.clear();
	// }
	private static PConcept getCachedConvertAndAbsorb(Concept kc,
			TBox convertedTb, boolean absorb) {
		PConcept pc = cachedConverts.get(kc);
		if (pc == null) {
//			pc = PConcept.newInternalPConcept();
			pc = PConcept.newInternalPConcept(kc);
			insertCachedConvert(kc, pc);
			if (absorb) {
				unaryAbsorb(pc, kc, convertedTb);
			}
		}
		return pc;
	}

	private static void insertCachedConvert(Concept kc, PConcept nc) {
		if (cachedConverts.containsKey(kc)) {
			System.out.println("Already found " + kc
					+ " as in the converted concepts.");
		}
		cachedConverts.put(kc, nc);
	}

	// assume C is in NNF.
	//true if you want new pconcept to be introduced for universals.
	private static Concept convertUniversal(UniversalConcept uc, boolean getNewName, TBox convertedTb) throws CoreReasoningException{
		Role r = uc.getRole();
		Concept filler = uc.getFiller();
		Concept nf = null;
		if (filler.isLiteral()) {
			nf = filler;
		} else {
			Concept rhs = convertConcept(filler, true, convertedTb);
			nf = getCachedConvertAndAbsorb(rhs, convertedTb, true);
		}
		UniversalConcept fr = new UniversalConcept(r, nf);
		if(getNewName){
			//return a new name
			PConcept nc = getCachedConvertAndAbsorb(fr, convertedTb, true);
			tboxGuardIntroduction(nc, r, nf, convertedTb);
			collectUniversals(nc, fr);
			return nc;
		}else{
			//return this new universal 
			return fr;
		}
	}
	
	private static Concept convertExists(ExistsConcept ec, boolean getNewName, TBox convertedTb) 
			throws CoreReasoningException{
		Role r = ec.getRole();
		Concept filler = ec.getFiller();
		Concept nf = null;
		boolean canAdd = false;
		if (filler.isLiteral()) {
			nf = filler;
			if(OptimizedExistentials.hasSomeIndividual(filler)){
				canAdd = true;
			}
		} else {
			Concept rhs = convertConcept(filler, true, convertedTb);
			if(OptimizedExistentials.hasSomeIndividual(rhs)){
				canAdd = true;
			}
			nf = getCachedConvertAndAbsorb(rhs, convertedTb, true);
		}
		ExistsConcept ne = new ExistsConcept(r, nf);
		//add auxiliary data, e.g., a':nf, unless it is known that some b:nf is in Abox
		if(canAdd){
			OptimizedExistentials.addNewABoxData(nf);
		}
		if(getNewName){
			//return a new name
			PConcept nc = getCachedConvertAndAbsorb(ne, convertedTb, true);
			collectExists(nc, ne);
			return nc;
		}else{
			//return this new universal 
			return ne;
		}
	}
	
	private static Concept convertConcept(Concept c, boolean getNewName,
			TBox convertedTb) throws CoreReasoningException {
		if (c instanceof NaryConcept) {
			Set<Concept> ac = new HashSet<Concept>();
			for (Concept cc : ((NaryConcept) c).getConceptSet()) {
				ac.add(convertConcept(cc, getNewName, convertedTb));
			}
			Concept naryc = null;
			if(c instanceof AndConcept){
				naryc = new AndConcept(ac);
			}else if(c instanceof OrConcept){
				naryc = new OrConcept(ac);
			}
			return naryc;
		} else if (c instanceof ExistsConcept) {
			if(OptimizedRestrictions.OptimizeEx){
				return convertExists((ExistsConcept) c, getNewName, convertedTb);
			}else{
				Role r = ((ExistsConcept) c).getRole();
				Concept filler = ((ExistsConcept) c).getFiller();
				ExistsConcept ec = new ExistsConcept(r, convertConcept(
						filler, getNewName, convertedTb));
				return ec;
			}
		} else if (c instanceof UniversalConcept) {
			return convertUniversal((UniversalConcept) c,  getNewName, convertedTb);
		} else if (c instanceof NotConcept) {
			NotConcept nc = (NotConcept) c;
			Concept fil = nc.getConcept();
			if (fil.isBot() || fil.isTop() || fil instanceof PConcept) {
				return nc;
			}
			throw new CoreReasoningException("The concept to be converted is not in NNF:"+c);
		} else {
			if (Completion.fullyGuardedReasoning
					&& !Completion.featureGuardsInRule
					&& c instanceof DomainConcept
					&& !definedFeatures.contains(c)) {
				for (Role f : c.extractFeatures()) {
					addGCI(c, PConcept.newGuardPConcept(f), convertedTb);
					definedFeatures.add((DomainConcept<?, ?>) c);
				}
			}
			return c;
		}
	}

	private static boolean validUseOfUniversal(Concept u) {
		if (u instanceof UniversalConcept) {
			UniversalConcept uc = (UniversalConcept) u;
			return uc.getFiller().isLiteral();
		}
		return false;
	}
	
	private static boolean validUseOfExists(Concept e) {
		if (e instanceof ExistsConcept) {
			ExistsConcept ec = (ExistsConcept) e;
			return ec.getFiller().isLiteral();
		}
		return false;
	}



	/*
	 * add TBox conversion directly here i.e., for A-> All R.B add A->DEFr
	 * ~B->DEFr^
	 */
	private static void tboxGuardIntroduction(Concept lhs, Role r,
			Concept filler, TBox convertedTb) {
		PConcept defr = PConcept.newGuardPConcept(r);
		Role ir = convertedTb.getRoleBox().getInverseRole(r);
		PConcept defir = PConcept.newGuardPConcept(ir);
		if (lhs.isTop()) {
			addGCI(KBVocabulary.CONCEPT_TOP, defr, convertedTb);
		} else if (lhs instanceof AtomicConcept) {
			// System.err.println(lhs+" -> "+defr);
			unaryAbsorb((AtomicConcept) lhs, defr, convertedTb);
		} else {
//			addGCI(preprocessor.Simplification.NNF(lhs, false), defr,
//					convertedTb);
			addGCI(lhs, defr,
					convertedTb);
		}
		// adding ~rhs -> DEF_r^ or GCI
		if (filler.isSimpleNot()) {
			NotConcept nc = (NotConcept) filler;
			unaryAbsorb((AtomicConcept) nc.getConcept(), defir, convertedTb);
		} else {
			// add as GCI
			boolean added = false;
			if (filler instanceof NotConcept) {
				NotConcept not = (NotConcept) filler;
				if (not.getConcept().isTop()) {
					addGCI(KBVocabulary.CONCEPT_TOP, defir, convertedTb);
					added = true;
				} else if (not.getConcept().isBot()) {
					// can be ignored as ~bot or A becomes bot -> A: trivial
					added = true;
				}
			}
			if (!added) {
				// System.out.println(filler +" -> "+defir);
				addGCI(new NotConcept(filler), defir, convertedTb);
			}
		}
	}

	// private void convertAssertion(Assertion ast) throws TypeException{
	// if(ast instanceof ConceptAssertion){
	// this.convertCAssertion((ConceptAssertion) ast);
	// }else if(ast instanceof RoleAssertion){
	// this.convertRAssertion((RoleAssertion) ast);
	// }else{
	// throw new TypeException("Unknown assertiont type.");
	// }
	// }

	private static void convertRAssertion(Individual a, Role r, Individual b,
			TBox convertedTb) {
		// if(Absorption.RA){
		// //extended role absorption on role assertions
		// RoleAbsorption.cacheRA(r, a, b);
		// }
		Nominal na = Nominal.getNominal(a.getName(), false);
		PConcept defa = PConcept.newGuardPConcept(na);
		Nominal nb = Nominal.getNominal(b.getName(), false);
		PConcept defb = PConcept.newGuardPConcept(nb);
		PConcept defr = PConcept.newGuardPConcept(r);
		Role ir = convertedTb.getRoleBox().getInverseRole(r);
		PConcept defir = PConcept.newGuardPConcept(ir);
		boolean skip = false;
//		if (OptimizedUniversals.OptimizeUR) {
//			if (OptimizedUniversals.skip(r, a, b)) {
//				skippedRAs++;
//				skip = true;
//			}
//		}
		if (!skip) {
			// if this RA can be skipped, do not introduce defb, nor {b}
			binaryAbsorb(na, defr, new ExistsConcept(r,
					new AndConcept(nb, defb)), convertedTb);
			if(addDomainRestrictionInBinaryPairs){
				Concept dom = new ExistsConcept(r, KBVocabulary.CONCEPT_TOP);
				binaryAbsorb(na, defa, dom, convertedTb);
			}
		}
		boolean skipbk = false;
//		if (OptimizedUniversals.OptimizeUR) {
//			if (OptimizedUniversals.skip(ir, b, a)) {
//				skippedRAs++;
//				skipbk = true;
//			}
//		}
		if (!skipbk) {
			binaryAbsorb(nb, defir, new ExistsConcept(ir, new AndConcept(na,
					defa)), convertedTb);
			if(addDomainRestrictionInBinaryPairs){
				Concept dombk = new ExistsConcept(ir, KBVocabulary.CONCEPT_TOP);
				binaryAbsorb(nb, defb, dombk, convertedTb);
			}
		}
	}

	// private void convertRAssertion(RoleAssertion ra){
	// Individual a = ra.getFirstIndividual();
	// Individual b = ra.getSecondIndividual();
	// Role r = ra.getRole();
	// this.convertRAssertion(a, r, b);
	// }

	public static void convertCAssertion(Individual a, Concept c,
			TBox convertedTb) throws TypeException, CoreReasoningException {
		if (c.isTop()) {
			return;
		}
		if (c.isBot()) {
			throw new TypeException("Inconsistent assertion given: " + a + c);
		}
		if(OptimizedRestrictions.OptimizeUR || OptimizedRestrictions.OptimizeEx){
			//add to index
			OptimizedRestrictions.addRealizedInd(c, a);
		}
		Nominal na = Nominal.getNominal(a.getName(), false);
		PConcept defa = PConcept.newGuardPConcept(na);
		for (Concept norm : normalizedABoxConcept(c, convertedTb)) {
			if (norm instanceof PConcept) {
				binaryAbsorb(na, defa, norm, convertedTb);
			} else if (norm instanceof DomainConcept) {
				if (Completion.fullyGuardedReasoning) {
					// if features are guarded, then binary (a and DEFf)->f op k
					DomainConcept<?, ?> dc = (DomainConcept<?, ?>) norm;
					Role f = (Role) dc.getRealFeature();
					PConcept deff = PConcept.newGuardPConcept(f);
					binaryAbsorb(na, deff, norm, convertedTb);
				} else if (Completion.partiallyGuardedReasoning) {
					// if features are not guarded, then unary absorption: a ->
					// f op k
					unaryAbsorb(na, norm, convertedTb);
				}

			} else {
				throw new TypeException("Incorrect assertion normalization:"
						+ c);
			}
		}
	}

	// private void convertCAssertion(ConceptAssertion ca) throws TypeException{
	// Individual a = ca.getIndividual();
	// Concept c = ca.getConcept();
	// this.convertCAssertion(a, c);
	// }

	/*
	 * Only allows: a:A; a:f op k; a: conjunction of these two; newly introduced
	 * A will be directly absorbed by unary absorption.
	 */
	private static Set<Concept> normalizedABoxConcept(Concept c,
			TBox convertedTb) throws CoreReasoningException {
		Set<Concept> ret = new HashSet<Concept>();
		if (c instanceof PConcept) {
			ret.add(c);
		} else if (c.isStandardDomainConcept()) {
			// do not accept (f op g) or (k1 op k2)
			ret.add(c);
		} else if (c instanceof AndConcept) {
			for (Concept d : ((AndConcept) c).getConceptSet()) {
				ret.addAll(normalizedABoxConcept(d, convertedTb));
			}
		} else {
			// for other concepts, introduce a fresh concept
			Concept processed = Simplification.NNF(c, false);
			processed = convertConcept(processed, true, convertedTb);
			ret.add(processed);
		}
		return ret;
	}

	private static void unaryAbsorb(AtomicConcept lhs, Concept rhs,
			TBox convertedTb) {
		try {
			convertedTb.insertTu(lhs, rhs);
		} catch (ConceptException e) {
			e.printStackTrace();
		}
	}

	private static Map<Concept, Set<Concept>> DefGCIs = new HashMap<Concept, Set<Concept>>();

	private static void addGCI(Concept lhs, Concept rhs, TBox convertedTb) {
		if (DefGCIs.containsKey(lhs)) {
			DefGCIs.get(lhs).add(rhs);
		} else {
			Set<Concept> vs = new HashSet<Concept>();
			vs.add(rhs);
			DefGCIs.put(lhs, vs);
		}
		// convertedTb.insertTg(lhs, rhs);
	}

	private static void addGCIToConvertedTb(TBox convertedTb) {
		for (Concept lhs : DefGCIs.keySet()) {
			Concept rhs = null;
			if (DefGCIs.get(lhs).size() >= 2) {
				rhs = new AndConcept(DefGCIs.get(lhs));
			} else {
				rhs = DefGCIs.get(lhs).iterator().next();
			}
			convertedTb.insertTg(lhs, rhs);
		}
	}

	public static void binaryAbsorb(AtomicConcept a, AtomicConcept def,
			Concept rhs, TBox convertedTb) {
		// we apply the limited version of binary absorption, i.e., {a} and DEF
		// -> C only
		try {
			convertedTb.getSpecialBinaryClass().addBinaryEntry(a, def, rhs);
		} catch (AbsorptionException e) {
			e.printStackTrace();
		}
	}
	
	//record all universals in use, e.g., ~A->all R.~B
	private static void collectUniversals(Concept lhs, UniversalConcept rhs){
		if(!OptimizedRestrictions.OptimizeUR){
			return;
		}
		OptimizedUniversals.addUniversal(lhs, rhs);
	}
	
	//collect existentials
	private static void collectExists(Concept lhs, ExistsConcept rhs){
		if(!OptimizedRestrictions.OptimizeEx){
			return;
		}
//		OptimizedExistentials.incCountEx();
		//filter the exists that cannot be guarded
//		Concept filler = rhs.getFiller();
//		if(filler.isTop() || OptimizedRestrictions.realizedInds.containsKey(filler)){
			OptimizedExistentials.addExists(lhs, rhs);
//		}
		
	}

}
